Option type

For families of option contracts in finance, see Option style.

In programming languages (especially functional programming languages) and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value; e.g. it is used as the return type of functions which may or may not return a meaningful value when they're applied. It consists of either an empty constructor (called None or Nothing), or a constructor encapsulating the original data type A (written Just A or Some A).

In the Haskell language, the option type (called Maybe) is defined as data Maybe a = Just a | Nothing. In the OCaml language, the option type is defined as type 'a option = None | Some of 'a. In the Scala language, Option is defined as parametrized abstract class '.. Option[A] = if (x == null) None else Some(x)... In the Standard ML language, the option type is defined as datatype 'a option = NONE | SOME of 'a.

In type theory, it may be written as: A^{?} = A %2B 1.

In languages that have tagged unions, as in most functional programming languages, option types can be expressed as the tagged union of a unit type plus the encapsulated type.

In the Curry-Howard correspondence, option types are related to the annihilation law for ∨: x∨1=1.

An option type can also be seen as a collection containing either a single element or zero elements.

Contents

The option monad

The option type is a monad under the following functions:

\text{return}\colon A \to A^{?} = a \mapsto \text{Just} \, a
\text{bind}\colon A^{?} \to (A \to B^{?}) \to B^{?} = a \mapsto f \mapsto \begin{cases} \text{Nothing} & \text{if} \ a = \text{Nothing}\\ f \, a' & \text{if} \ a = \text{Just} \, a' \end{cases}

We may also describe the option monad in terms of functions return, fmap and join, where the latter two are given by:

\text{fmap} \colon (A \to B) \to (A^{?} \to B^{?}) = f \mapsto a \mapsto \begin{cases} \text{Nothing} & \text{if} \ a = \text{Nothing}\\ \text{Just} \, f \, a' & \text{if} \ a = \text{Just} \, a' \end{cases}
\text{join} \colon {A^{?}}^{?} \to A^{?} = a \mapsto \begin{cases} \text{Nothing} & \text{if} \ a = \text{Nothing}\\ \text{Nothing} & \text{if} \ a = \text{Just} \, \text{Nothing}\\ \text{Just} \, a' & \text{if} \ a = \text{Just} \, \text{Just} \, a' \end{cases}

The option monad is an additive monad: it has Nothing as a zero constructor and the following function as a monadic sum:

\text{mplus} \colon A^{?} \to A^{?} \to A^{?} = a_1 \mapsto a_2 \mapsto \begin{cases} \text{Nothing} & \text{if} \ a_1 = \text{Nothing} \and a_2 = \text{Nothing}\\ \text{Just} \, a'_2 & \text{if} \ a_1 = \text{Nothing} \and a_2 = \text{Just} \, a'_2 \\ \text{Just} \, a'_1 & \text{if} \ a_1 = \text{Just} \, a'_1 \end{cases}

In fact, the resulting structure is an idempotent monoid.

Examples

Scala

Scala implements the Option type using Java generics, so you can specify the type of a variable as an Option and then access it as follows:[1]

class Person(val name: String, val age: Int)
 
var mightBeAPerson: Option[Person] = None
 
mightBeAPerson.isDefined // false
 
mightBeAPerson = Some(Person("Fred Flintstone", 50))
 
mightBeAPerson.isDefined // true
 
mightBeAPerson.get // returns the object

It essentially works as a type-safe alternative to the null value.

See also

References

  1. ^ Martin Odersky; Lex Spoon; Bill Venners (2008). Programming in Scala. Artima Inc. pp. 282–284. ISBN 978-0-9815316-0-1. http://books.google.com/books?id=MFjNhTjeQKkC&pg=PA283. Retrieved 6 September 2011. 
Uninterpreted
Numeric
Text
Pointer
Composite
Other
Related topics